%We also make use of the concept of monadic and biadic context.
The following notion of \emph{monadic and biadic contexts} will be useful in proofs.

\begin{definition}[Monadic and Biadic  Contexts]\label{d:mc}
A \emph{monadic  context} is a context with one hole (denoted ``$\cdot$'') and is defined according to the following grammar: 
$$
C[\cdot]::= [\cdot] \midd C[\cdot] \parallel P  \midd    \componentbbig{a}{C[\cdot]  } 
$$
where $P$ is  an \evol{} process. Similarly, a \emph{biadic context} is a context with two holes 
(denoted ``$\cdot_{1}$'' and ``$\cdot_{2}$'', respectively)
defined according to the following grammar: 
$$
D[\cdot_{1},\cdot_{2}]::= C[\cdot_{1}] \parallel C[\cdot_{2}]  \midd  \componentbbig{a}{D[\cdot_{1},\cdot_{2}] } \parallel P \midd \componentbbig{a}{D[\cdot_{1},\cdot_{2}] }
$$
where $P$ is an \evol{} process and $C$ is a monadic context.
As customary, $C[P]$ and $D[R,Q]$ represent the processes obtained by replacing the holes in contexts $C[\cdot]$ and $D[\cdot_{1},\cdot_{2}]$
with processes $P$ and $R,Q$, respectively.
\end{definition}

